package il.ac.technion.cs236700.utils.DBC;

import il.ac.technion.cs236700.utils.Log;
import il.ac.technion.cs236700.utils.STOP;

import java.util.Formatter;


/**
 * A simple implementation of design by contract. Violations are reported to
 * <code>System.err</code.>. Error descriptions are passed by a <code>printf</code> 
 * like argument syntax. Often used with static import.
 */
public enum DBC {
	// A namespace: no values to this enum
	;
	/**  Exercise the {@link Checkable#invariant()}
	 * @param c
	 */
	public static void checkInvariant(Checkable c) {
		try {
			c.toString();
		} catch (Throwable t) {
			// Absorb
		}
		c.invariant();
	}

	/**
	 * A possibly non-returning method to be used for checking pre-conditions.
	 * 
	 * @param cond
	 *            if <code><b>false</b></code>, program will halt.
	 * @param args
	 *            a list of strings in a <code>printf</code> like format
	 *            describing the violation.
	 */
	public static void require(boolean cond, String... args) {
		error(cond, "Requirement not met", args);
	}

	public static void warn(boolean cond, String s) {
		if (cond)
			return;
		System.out.println(s);
	}

	/**
	 * A possibly non-returning method to be used for checking post-conditions.
	 * 
	 * @param cond
	 *            if <code><b>false</b></code>, program will halt.
	 * @param args
	 *            a list of strings in a <code>printf</code> like format
	 *            describing the violation.
	 */
	public static void ensure(boolean cond, String... args) {
		error(cond, "Promise not kept", args);
	}

	/**
	 * A never-returning method to be used in points of code which should never
	 * be reached.
	 * 
	 * @param args
	 *            a list of strings in a <code>printf</code> like format
	 *            describing the violation.
	 */
	public static void unreachable(String... args) {
		error("This point in the code should never be reached", args);
	}

	/**
	 * A possibly non-returning method to be used for checking assertions.
	 * 
	 * @param cond
	 *            If <code><b>false</b></code>, then the condition is violated and execution
	 *            terminates with an error report.
	 * @param args
	 *            a list of strings in a <code>printf</code> like format
	 *            describing the violation.
	 */
	public static void sure(boolean cond, String... args) {
		error(cond, "Assumption failed", args);
	}

	/**
	 * A never-returning method indicating code sites with missing functionality
	 * 
	 * @param args
	 *            a list of strings in a <code>printf</code> like format
	 *            describing the task to be done.
	 */
	public static void todo(String... args) {
		error("Feature unsupported. ", args);
	}

	/**
	 * A class to emulate Eiffel's <code>variant</code> construct.
	 * <p>
	 * To use, create an object of this type, and then call function
	 * {@link #check(int)} successively.
	 * 
	 * @author Yossi Gil <yogi@cs.technion.ac.il> 
	 * @date 05/06/2007
	 */
	static public final class Variant {
		private int value;

		Variant(int value) {
			error(value < 0, "Initial value of variannt (%d) is negative", box(value));
			this.value = value;
		}

		void check(int new_value) {
			error(new_value >= value, "New variant value (%d) should be less than previous value (%d)", box(new_value), box(value));
			error(new_value < 0, "New variant value (%d) is negative", box(new_value));
			value = new_value;
		}

		private static String box(int n) {
			return "" + n;
		}
	}

	/**
	 * A possibly non returning method used in class implementation.
	 * 
	 * @param cond
	 *            If <code><b>false</b></code>, method will not return and
	 *            print error message.
	 * @param kind
	 *            A string describing the error kind, e.g., pre-condition
	 *            failure
	 * @param args
	 *            Additional stings describing the error kind in a
	 *            <code>printf</code> format.
	 */
	static void error(boolean cond, String kind, String... args) {
		if (cond)
			return;
		error(kind, args);
	}

	private static void error(String kind, String... args) {
		String s = buildMessage(kind, args);
		System.out.flush();
		System.err.flush();
		System.err.println(s);
		System.err.flush();
		Log.printStackTrace();
		STOP.stop(-1);
	}

	public static String sprintf(String format, String... args) {
		Formatter f = new Formatter();
		Object os[] = args;
		f.format(format, os);
		return f.toString();
	}

	public static String buildMessage(String kind, String... args) {
		String $ = kind + " ";
		switch (args.length) {
			case 0:
				break;
			case 1:
				$ += args[0];
				break;
			default:
				Object os[] = new Object[args.length - 1];
				for (int i = 1; i < args.length; i++)
					os[i - 1] = args[i];
				Formatter f = new Formatter();
				f.format(args[0], os);
				$ += f.out();
		}
		return $;
	}
}
